Nuprl Lemma : q-rel_wf
11,40
postcript
pdf
r
:
,
x
:
. q-rel(
r
;
x
)
latex
Definitions
q-rel(
r
;
x
)
,
,
t
T
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
qless
wf
,
qle
wf
,
int
inc
rationals
,
rationals
wf
,
eq
int
wf
,
ifthenelse
wf
origin
r:
, x:
. q-rel(r;x) 
r:, x:. q-rel(r;x) Tx:A. B(x)
T